Metamath Proof Explorer

Theorem fin2so

Description: Any totally ordered Tarski-finite set is finite; in particular, no amorphous set can be ordered. Theorem 2 of [Levy58] p. 4. (Contributed by Brendan Leahy, 28-Jun-2019)

Ref Expression
Assertion fin2so ( ( 𝐴 ∈ FinII ∧ 𝑅 Or 𝐴 ) → 𝐴 ∈ Fin )

Proof

Step Hyp Ref Expression
1 simplll ⊢ ( ( ( ( 𝐴 ∈ FinII ∧ 𝑅 Or 𝐴 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ 𝑥 ≠ ∅ ) → 𝐴 ∈ FinII )
2 ssrab2 ⊢ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ⊆ 𝑥
3 sstr ⊢ ( ( { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ⊆ 𝐴 )
4 2 3 mpan ⊢ ( 𝑥 ⊆ 𝐴 → { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ⊆ 𝐴 )
5 elpw2g ⊢ ( 𝐴 ∈ FinII → ( { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ∈ 𝒫 𝐴 ↔ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ⊆ 𝐴 ) )
6 5 biimpar ⊢ ( ( 𝐴 ∈ FinII ∧ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ⊆ 𝐴 ) → { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ∈ 𝒫 𝐴 )
7 4 6 sylan2 ⊢ ( ( 𝐴 ∈ FinII ∧ 𝑥 ⊆ 𝐴 ) → { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ∈ 𝒫 𝐴 )
8 7 ralrimivw ⊢ ( ( 𝐴 ∈ FinII ∧ 𝑥 ⊆ 𝐴 ) → ∀ 𝑣 ∈ 𝑥 { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ∈ 𝒫 𝐴 )
9 vex ⊢ 𝑥 ∈ V
10 9 rabex ⊢ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ∈ V
11 10 rgenw ⊢ ∀ 𝑣 ∈ 𝑥 { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ∈ V
12 eqid ⊢ ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) = ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } )
13 eleq1 ⊢ ( 𝑦 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } → ( 𝑦 ∈ 𝒫 𝐴 ↔ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ∈ 𝒫 𝐴 ) )
14 12 13 ralrnmptw ⊢ ( ∀ 𝑣 ∈ 𝑥 { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ∈ V → ( ∀ 𝑦 ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) 𝑦 ∈ 𝒫 𝐴 ↔ ∀ 𝑣 ∈ 𝑥 { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ∈ 𝒫 𝐴 ) )
15 11 14 ax-mp ⊢ ( ∀ 𝑦 ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) 𝑦 ∈ 𝒫 𝐴 ↔ ∀ 𝑣 ∈ 𝑥 { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ∈ 𝒫 𝐴 )
16 8 15 sylibr ⊢ ( ( 𝐴 ∈ FinII ∧ 𝑥 ⊆ 𝐴 ) → ∀ 𝑦 ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) 𝑦 ∈ 𝒫 𝐴 )
17 dfss3 ⊢ ( ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ⊆ 𝒫 𝐴 ↔ ∀ 𝑦 ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) 𝑦 ∈ 𝒫 𝐴 )
18 16 17 sylibr ⊢ ( ( 𝐴 ∈ FinII ∧ 𝑥 ⊆ 𝐴 ) → ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ⊆ 𝒫 𝐴 )
19 18 adantlr ⊢ ( ( ( 𝐴 ∈ FinII ∧ 𝑅 Or 𝐴 ) ∧ 𝑥 ⊆ 𝐴 ) → ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ⊆ 𝒫 𝐴 )
20 19 adantr ⊢ ( ( ( ( 𝐴 ∈ FinII ∧ 𝑅 Or 𝐴 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ 𝑥 ≠ ∅ ) → ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ⊆ 𝒫 𝐴 )
21 10 12 dmmpti ⊢ dom ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) = 𝑥
22 21 neeq1i ⊢ ( dom ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ≠ ∅ ↔ 𝑥 ≠ ∅ )
23 dm0rn0 ⊢ ( dom ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) = ∅ ↔ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) = ∅ )
24 23 necon3bii ⊢ ( dom ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ≠ ∅ ↔ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ≠ ∅ )
25 22 24 sylbb1 ⊢ ( 𝑥 ≠ ∅ → ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ≠ ∅ )
26 25 adantl ⊢ ( ( ( ( 𝐴 ∈ FinII ∧ 𝑅 Or 𝐴 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ 𝑥 ≠ ∅ ) → ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ≠ ∅ )
27 soss ⊢ ( 𝑥 ⊆ 𝐴 → ( 𝑅 Or 𝐴 → 𝑅 Or 𝑥 ) )
28 27 impcom ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴 ) → 𝑅 Or 𝑥 )
29 porpss ⊢ [⊊] Po ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } )
30 29 a1i ⊢ ( 𝑅 Or 𝑥 → [⊊] Po ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) )
31 solin ⊢ ( ( 𝑅 Or 𝑥 ∧ ( 𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥 ) ) → ( 𝑣 𝑅 𝑦 ∨ 𝑣 = 𝑦 ∨ 𝑦 𝑅 𝑣 ) )
32 fin2solem ⊢ ( ( 𝑅 Or 𝑥 ∧ ( 𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥 ) ) → ( 𝑣 𝑅 𝑦 → { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ) )
33 breq2 ⊢ ( 𝑣 = 𝑦 → ( 𝑤 𝑅 𝑣 ↔ 𝑤 𝑅 𝑦 ) )
34 33 rabbidv ⊢ ( 𝑣 = 𝑦 → { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } )
35 34 a1i ⊢ ( ( 𝑅 Or 𝑥 ∧ ( 𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥 ) ) → ( 𝑣 = 𝑦 → { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ) )
36 fin2solem ⊢ ( ( 𝑅 Or 𝑥 ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥 ) ) → ( 𝑦 𝑅 𝑣 → { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) )
37 36 ancom2s ⊢ ( ( 𝑅 Or 𝑥 ∧ ( 𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥 ) ) → ( 𝑦 𝑅 𝑣 → { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) )
38 32 35 37 3orim123d ⊢ ( ( 𝑅 Or 𝑥 ∧ ( 𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥 ) ) → ( ( 𝑣 𝑅 𝑦 ∨ 𝑣 = 𝑦 ∨ 𝑦 𝑅 𝑣 ) → ( { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ) )
39 31 38 mpd ⊢ ( ( 𝑅 Or 𝑥 ∧ ( 𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥 ) ) → ( { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) )
40 39 ralrimivva ⊢ ( 𝑅 Or 𝑥 → ∀ 𝑣 ∈ 𝑥 ∀ 𝑦 ∈ 𝑥 ( { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) )
41 breq1 ⊢ ( 𝑢 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } → ( 𝑢 [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ↔ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ) )
42 eqeq1 ⊢ ( 𝑢 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } → ( 𝑢 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ↔ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ) )
43 breq2 ⊢ ( 𝑢 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } → ( { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] 𝑢 ↔ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) )
44 41 42 43 3orbi123d ⊢ ( 𝑢 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } → ( ( 𝑢 [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ 𝑢 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] 𝑢 ) ↔ ( { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ) )
45 44 ralbidv ⊢ ( 𝑢 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } → ( ∀ 𝑦 ∈ 𝑥 ( 𝑢 [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ 𝑢 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] 𝑢 ) ↔ ∀ 𝑦 ∈ 𝑥 ( { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ) )
46 12 45 ralrnmptw ⊢ ( ∀ 𝑣 ∈ 𝑥 { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ∈ V → ( ∀ 𝑢 ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ∀ 𝑦 ∈ 𝑥 ( 𝑢 [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ 𝑢 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] 𝑢 ) ↔ ∀ 𝑣 ∈ 𝑥 ∀ 𝑦 ∈ 𝑥 ( { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ) )
47 11 46 ax-mp ⊢ ( ∀ 𝑢 ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ∀ 𝑦 ∈ 𝑥 ( 𝑢 [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ 𝑢 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] 𝑢 ) ↔ ∀ 𝑣 ∈ 𝑥 ∀ 𝑦 ∈ 𝑥 ( { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) )
48 40 47 sylibr ⊢ ( 𝑅 Or 𝑥 → ∀ 𝑢 ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ∀ 𝑦 ∈ 𝑥 ( 𝑢 [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ 𝑢 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] 𝑢 ) )
49 48 r19.21bi ⊢ ( ( 𝑅 Or 𝑥 ∧ 𝑢 ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ) → ∀ 𝑦 ∈ 𝑥 ( 𝑢 [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ 𝑢 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] 𝑢 ) )
50 9 rabex ⊢ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∈ V
51 50 rgenw ⊢ ∀ 𝑦 ∈ 𝑥 { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∈ V
52 34 cbvmptv ⊢ ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) = ( 𝑦 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } )
53 breq2 ⊢ ( 𝑧 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } → ( 𝑢 [⊊] 𝑧 ↔ 𝑢 [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ) )
54 eqeq2 ⊢ ( 𝑧 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } → ( 𝑢 = 𝑧 ↔ 𝑢 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ) )
55 breq1 ⊢ ( 𝑧 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } → ( 𝑧 [⊊] 𝑢 ↔ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] 𝑢 ) )
56 53 54 55 3orbi123d ⊢ ( 𝑧 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } → ( ( 𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢 ) ↔ ( 𝑢 [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ 𝑢 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] 𝑢 ) ) )
57 52 56 ralrnmptw ⊢ ( ∀ 𝑦 ∈ 𝑥 { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∈ V → ( ∀ 𝑧 ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ( 𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢 ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝑢 [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ 𝑢 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] 𝑢 ) ) )
58 51 57 ax-mp ⊢ ( ∀ 𝑧 ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ( 𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢 ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝑢 [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ 𝑢 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ∨ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] 𝑢 ) )
59 49 58 sylibr ⊢ ( ( 𝑅 Or 𝑥 ∧ 𝑢 ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ) → ∀ 𝑧 ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ( 𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢 ) )
60 59 r19.21bi ⊢ ( ( ( 𝑅 Or 𝑥 ∧ 𝑢 ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ) ∧ 𝑧 ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ) → ( 𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢 ) )
61 60 anasss ⊢ ( ( 𝑅 Or 𝑥 ∧ ( 𝑢 ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ∧ 𝑧 ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ) ) → ( 𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢 ) )
62 30 61 issod ⊢ ( 𝑅 Or 𝑥 → [⊊] Or ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) )
63 28 62 syl ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴 ) → [⊊] Or ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) )
64 63 adantll ⊢ ( ( ( 𝐴 ∈ FinII ∧ 𝑅 Or 𝐴 ) ∧ 𝑥 ⊆ 𝐴 ) → [⊊] Or ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) )
65 64 adantr ⊢ ( ( ( ( 𝐴 ∈ FinII ∧ 𝑅 Or 𝐴 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ 𝑥 ≠ ∅ ) → [⊊] Or ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) )
66 fin2i2 ⊢ ( ( ( 𝐴 ∈ FinII ∧ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ⊆ 𝒫 𝐴 ) ∧ ( ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ≠ ∅ ∧ [⊊] Or ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ) ) → ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) )
67 1 20 26 65 66 syl22anc ⊢ ( ( ( ( 𝐴 ∈ FinII ∧ 𝑅 Or 𝐴 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ 𝑥 ≠ ∅ ) → ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) )
68 52 50 elrnmpti ⊢ ( ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ↔ ∃ 𝑦 ∈ 𝑥 ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } )
69 67 68 sylib ⊢ ( ( ( ( 𝐴 ∈ FinII ∧ 𝑅 Or 𝐴 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } )
70 ssel2 ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → 𝑧 ∈ 𝐴 )
71 sonr ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ¬ 𝑧 𝑅 𝑧 )
72 70 71 sylan2 ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑧 ∈ 𝑥 ) ) → ¬ 𝑧 𝑅 𝑧 )
73 72 anassrs ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴 ) ∧ 𝑧 ∈ 𝑥 ) → ¬ 𝑧 𝑅 𝑧 )
74 73 adantlr ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝑥 ) → ¬ 𝑧 𝑅 𝑧 )
75 74 adantr ⊢ ( ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝑥 ) ∧ ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ) → ¬ 𝑧 𝑅 𝑧 )
76 breq1 ⊢ ( 𝑤 = 𝑧 → ( 𝑤 𝑅 𝑦 ↔ 𝑧 𝑅 𝑦 ) )
77 76 elrab ⊢ ( 𝑧 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑧 𝑅 𝑦 ) )
78 77 simplbi2 ⊢ ( 𝑧 ∈ 𝑥 → ( 𝑧 𝑅 𝑦 → 𝑧 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ) )
79 78 ad2antlr ⊢ ( ( ( 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ∧ ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ) → ( 𝑧 𝑅 𝑦 → 𝑧 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ) )
80 vex ⊢ 𝑧 ∈ V
81 80 elint2 ⊢ ( 𝑧 ∈ ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ↔ ∀ 𝑦 ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) 𝑧 ∈ 𝑦 )
82 eleq2 ⊢ ( 𝑦 = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) )
83 12 82 ralrnmptw ⊢ ( ∀ 𝑣 ∈ 𝑥 { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ∈ V → ( ∀ 𝑦 ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) 𝑧 ∈ 𝑦 ↔ ∀ 𝑣 ∈ 𝑥 𝑧 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) )
84 11 83 ax-mp ⊢ ( ∀ 𝑦 ∈ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) 𝑧 ∈ 𝑦 ↔ ∀ 𝑣 ∈ 𝑥 𝑧 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } )
85 81 84 bitri ⊢ ( 𝑧 ∈ ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ↔ ∀ 𝑣 ∈ 𝑥 𝑧 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } )
86 breq2 ⊢ ( 𝑣 = 𝑧 → ( 𝑤 𝑅 𝑣 ↔ 𝑤 𝑅 𝑧 ) )
87 86 rabbidv ⊢ ( 𝑣 = 𝑧 → { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } )
88 87 eleq2d ⊢ ( 𝑣 = 𝑧 → ( 𝑧 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ↔ 𝑧 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } ) )
89 88 rspcv ⊢ ( 𝑧 ∈ 𝑥 → ( ∀ 𝑣 ∈ 𝑥 𝑧 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } → 𝑧 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } ) )
90 breq1 ⊢ ( 𝑤 = 𝑧 → ( 𝑤 𝑅 𝑧 ↔ 𝑧 𝑅 𝑧 ) )
91 90 elrab ⊢ ( 𝑧 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑧 𝑅 𝑧 ) )
92 91 simprbi ⊢ ( 𝑧 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } → 𝑧 𝑅 𝑧 )
93 89 92 syl6 ⊢ ( 𝑧 ∈ 𝑥 → ( ∀ 𝑣 ∈ 𝑥 𝑧 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } → 𝑧 𝑅 𝑧 ) )
94 93 adantl ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) → ( ∀ 𝑣 ∈ 𝑥 𝑧 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } → 𝑧 𝑅 𝑧 ) )
95 85 94 biimtrid ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) → ( 𝑧 ∈ ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) → 𝑧 𝑅 𝑧 ) )
96 eleq2 ⊢ ( ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } → ( 𝑧 ∈ ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) ↔ 𝑧 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ) )
97 96 imbi1d ⊢ ( ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } → ( ( 𝑧 ∈ ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) → 𝑧 𝑅 𝑧 ) ↔ ( 𝑧 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } → 𝑧 𝑅 𝑧 ) ) )
98 95 97 syl5ibcom ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) → ( ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } → ( 𝑧 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } → 𝑧 𝑅 𝑧 ) ) )
99 98 imp ⊢ ( ( ( 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ∧ ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ) → ( 𝑧 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } → 𝑧 𝑅 𝑧 ) )
100 79 99 syld ⊢ ( ( ( 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ∧ ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ) → ( 𝑧 𝑅 𝑦 → 𝑧 𝑅 𝑧 ) )
101 100 adantlll ⊢ ( ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝑥 ) ∧ ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ) → ( 𝑧 𝑅 𝑦 → 𝑧 𝑅 𝑧 ) )
102 75 101 mtod ⊢ ( ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝑥 ) ∧ ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ) → ¬ 𝑧 𝑅 𝑦 )
103 102 ex ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝑥 ) → ( ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } → ¬ 𝑧 𝑅 𝑦 ) )
104 103 ralrimdva ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴 ) ∧ 𝑦 ∈ 𝑥 ) → ( ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } → ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
105 104 reximdva ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴 ) → ( ∃ 𝑦 ∈ 𝑥 ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
106 105 adantll ⊢ ( ( ( 𝐴 ∈ FinII ∧ 𝑅 Or 𝐴 ) ∧ 𝑥 ⊆ 𝐴 ) → ( ∃ 𝑦 ∈ 𝑥 ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
107 106 adantr ⊢ ( ( ( ( 𝐴 ∈ FinII ∧ 𝑅 Or 𝐴 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ 𝑥 ≠ ∅ ) → ( ∃ 𝑦 ∈ 𝑥 ∩ ran ( 𝑣 ∈ 𝑥 ↦ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑣 } ) = { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
108 69 107 mpd ⊢ ( ( ( ( 𝐴 ∈ FinII ∧ 𝑅 Or 𝐴 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 )
109 108 expl ⊢ ( ( 𝐴 ∈ FinII ∧ 𝑅 Or 𝐴 ) → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
110 109 alrimiv ⊢ ( ( 𝐴 ∈ FinII ∧ 𝑅 Or 𝐴 ) → ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
111 df-fr ⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )
112 110 111 sylibr ⊢ ( ( 𝐴 ∈ FinII ∧ 𝑅 Or 𝐴 ) → 𝑅 Fr 𝐴 )
113 simpr ⊢ ( ( 𝐴 ∈ FinII ∧ 𝑅 Or 𝐴 ) → 𝑅 Or 𝐴 )
114 df-we ⊢ ( 𝑅 We 𝐴 ↔ ( 𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴 ) )
115 112 113 114 sylanbrc ⊢ ( ( 𝐴 ∈ FinII ∧ 𝑅 Or 𝐴 ) → 𝑅 We 𝐴 )
116 weinxp ⊢ ( 𝑅 We 𝐴 ↔ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 )
117 115 116 sylib ⊢ ( ( 𝐴 ∈ FinII ∧ 𝑅 Or 𝐴 ) → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 )
118 sqxpexg ⊢ ( 𝐴 ∈ FinII → ( 𝐴 × 𝐴 ) ∈ V )
119 incom ⊢ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = ( ( 𝐴 × 𝐴 ) ∩ 𝑅 )
120 inex1g ⊢ ( ( 𝐴 × 𝐴 ) ∈ V → ( ( 𝐴 × 𝐴 ) ∩ 𝑅 ) ∈ V )
121 119 120 eqeltrid ⊢ ( ( 𝐴 × 𝐴 ) ∈ V → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V )
122 weeq1 ⊢ ( 𝑧 = ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) → ( 𝑧 We 𝐴 ↔ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 ) )
123 122 spcegv ⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V → ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 → ∃ 𝑧 𝑧 We 𝐴 ) )
124 118 121 123 3syl ⊢ ( 𝐴 ∈ FinII → ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 → ∃ 𝑧 𝑧 We 𝐴 ) )
125 124 imp ⊢ ( ( 𝐴 ∈ FinII ∧ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 ) → ∃ 𝑧 𝑧 We 𝐴 )
126 117 125 syldan ⊢ ( ( 𝐴 ∈ FinII ∧ 𝑅 Or 𝐴 ) → ∃ 𝑧 𝑧 We 𝐴 )
127 ween ⊢ ( 𝐴 ∈ dom card ↔ ∃ 𝑧 𝑧 We 𝐴 )
128 126 127 sylibr ⊢ ( ( 𝐴 ∈ FinII ∧ 𝑅 Or 𝐴 ) → 𝐴 ∈ dom card )
129 fin23 ⊢ ( 𝐴 ∈ FinII → 𝐴 ∈ FinIII )
130 fin34 ⊢ ( 𝐴 ∈ FinIII → 𝐴 ∈ FinIV )
131 fin45 ⊢ ( 𝐴 ∈ FinIV → 𝐴 ∈ FinV )
132 129 130 131 3syl ⊢ ( 𝐴 ∈ FinII → 𝐴 ∈ FinV )
133 fin56 ⊢ ( 𝐴 ∈ FinV → 𝐴 ∈ FinVI )
134 fin67 ⊢ ( 𝐴 ∈ FinVI → 𝐴 ∈ FinVII )
135 132 133 134 3syl ⊢ ( 𝐴 ∈ FinII → 𝐴 ∈ FinVII )
136 fin71num ⊢ ( 𝐴 ∈ dom card → ( 𝐴 ∈ FinVII ↔ 𝐴 ∈ Fin ) )
137 136 biimpac ⊢ ( ( 𝐴 ∈ FinVII ∧ 𝐴 ∈ dom card ) → 𝐴 ∈ Fin )
138 135 137 sylan ⊢ ( ( 𝐴 ∈ FinII ∧ 𝐴 ∈ dom card ) → 𝐴 ∈ Fin )
139 128 138 syldan ⊢ ( ( 𝐴 ∈ FinII ∧ 𝑅 Or 𝐴 ) → 𝐴 ∈ Fin )