Metamath Proof Explorer

Theorem acwer1prclem

Description: Lemma for acwer1prc . (Contributed by BTernaryTau, 31-Jul-2026)

Ref Expression
Hypothesis acwer1prclem.1 ⊢ 𝑊 = { 𝑟 ∣ ∃ 𝑥 ∈ On ( 𝑟 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑟 We ( 𝑅1 ‘ 𝑥 ) ) }
Assertion acwer1prclem ( ( CHOICE ∧ ω ≼ 𝐴 ∧ ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) = 𝐴 ) → ∃ 𝑠 ( ( card ‘ 𝑠 ) ∈ ( card “ 𝑊 ) ∧ ( card ‘ 𝑠 ) = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 acwer1prclem.1 ⊢ 𝑊 = { 𝑟 ∣ ∃ 𝑥 ∈ On ( 𝑟 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑟 We ( 𝑅1 ‘ 𝑥 ) ) }
2 simp1 ⊢ ( ( CHOICE ∧ ω ≼ 𝐴 ∧ ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) = 𝐴 ) → CHOICE )
3 breq2 ⊢ ( ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) = 𝐴 → ( ω ≼ ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) ↔ ω ≼ 𝐴 ) )
4 3 biimpar ⊢ ( ( ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) = 𝐴 ∧ ω ≼ 𝐴 ) → ω ≼ ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) )
5 fvex ⊢ ( 𝑅1 ‘ 𝐵 ) ∈ V
6 acnum ⊢ ( CHOICE → ( ( 𝑅1 ‘ 𝐵 ) ∈ V → ( 𝑅1 ‘ 𝐵 ) ∈ dom card ) )
7 5 6 mpi ⊢ ( CHOICE → ( 𝑅1 ‘ 𝐵 ) ∈ dom card )
8 cardid2 ⊢ ( ( 𝑅1 ‘ 𝐵 ) ∈ dom card → ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) ≈ ( 𝑅1 ‘ 𝐵 ) )
9 domentr ⊢ ( ( ω ≼ ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) ∧ ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) ≈ ( 𝑅1 ‘ 𝐵 ) ) → ω ≼ ( 𝑅1 ‘ 𝐵 ) )
10 8 9 sylan2 ⊢ ( ( ω ≼ ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) ∧ ( 𝑅1 ‘ 𝐵 ) ∈ dom card ) → ω ≼ ( 𝑅1 ‘ 𝐵 ) )
11 7 10 sylan2 ⊢ ( ( ω ≼ ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) ∧ CHOICE ) → ω ≼ ( 𝑅1 ‘ 𝐵 ) )
12 11 expcom ⊢ ( CHOICE → ( ω ≼ ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) → ω ≼ ( 𝑅1 ‘ 𝐵 ) ) )
13 4 12 syl5 ⊢ ( CHOICE → ( ( ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) = 𝐴 ∧ ω ≼ 𝐴 ) → ω ≼ ( 𝑅1 ‘ 𝐵 ) ) )
14 13 ancomsd ⊢ ( CHOICE → ( ( ω ≼ 𝐴 ∧ ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) = 𝐴 ) → ω ≼ ( 𝑅1 ‘ 𝐵 ) ) )
15 14 3impib ⊢ ( ( CHOICE ∧ ω ≼ 𝐴 ∧ ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) = 𝐴 ) → ω ≼ ( 𝑅1 ‘ 𝐵 ) )
16 dfac8 ⊢ ( CHOICE ↔ ∀ 𝑧 ∃ 𝑦 𝑦 We 𝑧 )
17 weeq2 ⊢ ( 𝑧 = ( 𝑅1 ‘ 𝐵 ) → ( 𝑦 We 𝑧 ↔ 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) )
18 17 exbidv ⊢ ( 𝑧 = ( 𝑅1 ‘ 𝐵 ) → ( ∃ 𝑦 𝑦 We 𝑧 ↔ ∃ 𝑦 𝑦 We ( 𝑅1 ‘ 𝐵 ) ) )
19 5 18 spcv ⊢ ( ∀ 𝑧 ∃ 𝑦 𝑦 We 𝑧 → ∃ 𝑦 𝑦 We ( 𝑅1 ‘ 𝐵 ) )
20 16 19 sylbi ⊢ ( CHOICE → ∃ 𝑦 𝑦 We ( 𝑅1 ‘ 𝐵 ) )
21 weexenwe ⊢ ( ( ∃ 𝑦 𝑦 We ( 𝑅1 ‘ 𝐵 ) ∧ ω ≼ ( 𝑅1 ‘ 𝐵 ) ) → ∃ 𝑠 ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ∧ 𝑠 ≈ ( 𝑅1 ‘ 𝐵 ) ) )
22 20 21 sylan ⊢ ( ( CHOICE ∧ ω ≼ ( 𝑅1 ‘ 𝐵 ) ) → ∃ 𝑠 ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ∧ 𝑠 ≈ ( 𝑅1 ‘ 𝐵 ) ) )
23 carden2b ⊢ ( 𝑠 ≈ ( 𝑅1 ‘ 𝐵 ) → ( card ‘ 𝑠 ) = ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) )
24 23 3anim3i ⊢ ( ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ∧ 𝑠 ≈ ( 𝑅1 ‘ 𝐵 ) ) → ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ∧ ( card ‘ 𝑠 ) = ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) ) )
25 24 eximi ⊢ ( ∃ 𝑠 ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ∧ 𝑠 ≈ ( 𝑅1 ‘ 𝐵 ) ) → ∃ 𝑠 ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ∧ ( card ‘ 𝑠 ) = ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) ) )
26 22 25 syl ⊢ ( ( CHOICE ∧ ω ≼ ( 𝑅1 ‘ 𝐵 ) ) → ∃ 𝑠 ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ∧ ( card ‘ 𝑠 ) = ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) ) )
27 2 15 26 syl2anc ⊢ ( ( CHOICE ∧ ω ≼ 𝐴 ∧ ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) = 𝐴 ) → ∃ 𝑠 ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ∧ ( card ‘ 𝑠 ) = ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) ) )
28 df-3an ⊢ ( ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ∧ ( card ‘ 𝑠 ) = ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) ) ↔ ( ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ) ∧ ( card ‘ 𝑠 ) = ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) ) )
29 fveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝐵 ) )
30 29 sqxpeqd ⊢ ( 𝑥 = 𝐵 → ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) = ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) )
31 30 sseq2d ⊢ ( 𝑥 = 𝐵 → ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ↔ 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ) )
32 eqidd ⊢ ( 𝑥 = 𝐵 → 𝑠 = 𝑠 )
33 32 29 weeq12d ⊢ ( 𝑥 = 𝐵 → ( 𝑠 We ( 𝑅1 ‘ 𝑥 ) ↔ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ) )
34 31 33 anbi12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝑥 ) ) ↔ ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ) ) )
35 34 rspcev ⊢ ( ( 𝐵 ∈ On ∧ ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ) ) → ∃ 𝑥 ∈ On ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝑥 ) ) )
36 0elon ⊢ ∅ ∈ On
37 r1fnon ⊢ 𝑅1 Fn On
38 37 fndmi ⊢ dom 𝑅1 = On
39 38 eleq2i ⊢ ( 𝐵 ∈ dom 𝑅1 ↔ 𝐵 ∈ On )
40 ndmfv ⊢ ( ¬ 𝐵 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐵 ) = ∅ )
41 39 40 sylnbir ⊢ ( ¬ 𝐵 ∈ On → ( 𝑅1 ‘ 𝐵 ) = ∅ )
42 r10 ⊢ ( 𝑅1 ‘ ∅ ) = ∅
43 41 42 eqtr4di ⊢ ( ¬ 𝐵 ∈ On → ( 𝑅1 ‘ 𝐵 ) = ( 𝑅1 ‘ ∅ ) )
44 43 sqxpeqd ⊢ ( ¬ 𝐵 ∈ On → ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) = ( ( 𝑅1 ‘ ∅ ) × ( 𝑅1 ‘ ∅ ) ) )
45 44 sseq2d ⊢ ( ¬ 𝐵 ∈ On → ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ↔ 𝑠 ⊆ ( ( 𝑅1 ‘ ∅ ) × ( 𝑅1 ‘ ∅ ) ) ) )
46 eqidd ⊢ ( ¬ 𝐵 ∈ On → 𝑠 = 𝑠 )
47 46 43 weeq12d ⊢ ( ¬ 𝐵 ∈ On → ( 𝑠 We ( 𝑅1 ‘ 𝐵 ) ↔ 𝑠 We ( 𝑅1 ‘ ∅ ) ) )
48 45 47 anbi12d ⊢ ( ¬ 𝐵 ∈ On → ( ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ) ↔ ( 𝑠 ⊆ ( ( 𝑅1 ‘ ∅ ) × ( 𝑅1 ‘ ∅ ) ) ∧ 𝑠 We ( 𝑅1 ‘ ∅ ) ) ) )
49 48 biimpa ⊢ ( ( ¬ 𝐵 ∈ On ∧ ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ) ) → ( 𝑠 ⊆ ( ( 𝑅1 ‘ ∅ ) × ( 𝑅1 ‘ ∅ ) ) ∧ 𝑠 We ( 𝑅1 ‘ ∅ ) ) )
50 fveq2 ⊢ ( 𝑥 = ∅ → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ ∅ ) )
51 50 sqxpeqd ⊢ ( 𝑥 = ∅ → ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) = ( ( 𝑅1 ‘ ∅ ) × ( 𝑅1 ‘ ∅ ) ) )
52 51 sseq2d ⊢ ( 𝑥 = ∅ → ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ↔ 𝑠 ⊆ ( ( 𝑅1 ‘ ∅ ) × ( 𝑅1 ‘ ∅ ) ) ) )
53 eqidd ⊢ ( 𝑥 = ∅ → 𝑠 = 𝑠 )
54 53 50 weeq12d ⊢ ( 𝑥 = ∅ → ( 𝑠 We ( 𝑅1 ‘ 𝑥 ) ↔ 𝑠 We ( 𝑅1 ‘ ∅ ) ) )
55 52 54 anbi12d ⊢ ( 𝑥 = ∅ → ( ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝑥 ) ) ↔ ( 𝑠 ⊆ ( ( 𝑅1 ‘ ∅ ) × ( 𝑅1 ‘ ∅ ) ) ∧ 𝑠 We ( 𝑅1 ‘ ∅ ) ) ) )
56 55 rspcev ⊢ ( ( ∅ ∈ On ∧ ( 𝑠 ⊆ ( ( 𝑅1 ‘ ∅ ) × ( 𝑅1 ‘ ∅ ) ) ∧ 𝑠 We ( 𝑅1 ‘ ∅ ) ) ) → ∃ 𝑥 ∈ On ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝑥 ) ) )
57 36 49 56 sylancr ⊢ ( ( ¬ 𝐵 ∈ On ∧ ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ) ) → ∃ 𝑥 ∈ On ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝑥 ) ) )
58 35 57 pm2.61ian ⊢ ( ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ) → ∃ 𝑥 ∈ On ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝑥 ) ) )
59 vex ⊢ 𝑠 ∈ V
60 sseq1 ⊢ ( 𝑟 = 𝑠 → ( 𝑟 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ↔ 𝑠 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ) )
61 weeq1 ⊢ ( 𝑟 = 𝑠 → ( 𝑟 We ( 𝑅1 ‘ 𝑥 ) ↔ 𝑠 We ( 𝑅1 ‘ 𝑥 ) ) )
62 60 61 anbi12d ⊢ ( 𝑟 = 𝑠 → ( ( 𝑟 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑟 We ( 𝑅1 ‘ 𝑥 ) ) ↔ ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝑥 ) ) ) )
63 62 rexbidv ⊢ ( 𝑟 = 𝑠 → ( ∃ 𝑥 ∈ On ( 𝑟 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑟 We ( 𝑅1 ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∈ On ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝑥 ) ) ) )
64 59 63 1 elab2 ⊢ ( 𝑠 ∈ 𝑊 ↔ ∃ 𝑥 ∈ On ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝑥 ) ) )
65 58 64 sylibr ⊢ ( ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ) → 𝑠 ∈ 𝑊 )
66 acnum ⊢ ( CHOICE → ( 𝑠 ∈ 𝑊 → 𝑠 ∈ dom card ) )
67 cardf2 ⊢ card : { 𝑣 ∣ ∃ 𝑤 ∈ On 𝑤 ≈ 𝑣 } ⟶ On
68 ffun ⊢ ( card : { 𝑣 ∣ ∃ 𝑤 ∈ On 𝑤 ≈ 𝑣 } ⟶ On → Fun card )
69 67 68 ax-mp ⊢ Fun card
70 funfvima ⊢ ( ( Fun card ∧ 𝑠 ∈ dom card ) → ( 𝑠 ∈ 𝑊 → ( card ‘ 𝑠 ) ∈ ( card “ 𝑊 ) ) )
71 69 70 mpan ⊢ ( 𝑠 ∈ dom card → ( 𝑠 ∈ 𝑊 → ( card ‘ 𝑠 ) ∈ ( card “ 𝑊 ) ) )
72 66 71 syli ⊢ ( CHOICE → ( 𝑠 ∈ 𝑊 → ( card ‘ 𝑠 ) ∈ ( card “ 𝑊 ) ) )
73 eqtr ⊢ ( ( ( card ‘ 𝑠 ) = ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) ∧ ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) = 𝐴 ) → ( card ‘ 𝑠 ) = 𝐴 )
74 73 expcom ⊢ ( ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) = 𝐴 → ( ( card ‘ 𝑠 ) = ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) → ( card ‘ 𝑠 ) = 𝐴 ) )
75 72 74 im2anan9 ⊢ ( ( CHOICE ∧ ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) = 𝐴 ) → ( ( 𝑠 ∈ 𝑊 ∧ ( card ‘ 𝑠 ) = ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) ) → ( ( card ‘ 𝑠 ) ∈ ( card “ 𝑊 ) ∧ ( card ‘ 𝑠 ) = 𝐴 ) ) )
76 65 75 sylani ⊢ ( ( CHOICE ∧ ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) = 𝐴 ) → ( ( ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ) ∧ ( card ‘ 𝑠 ) = ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) ) → ( ( card ‘ 𝑠 ) ∈ ( card “ 𝑊 ) ∧ ( card ‘ 𝑠 ) = 𝐴 ) ) )
77 28 76 biimtrid ⊢ ( ( CHOICE ∧ ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) = 𝐴 ) → ( ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ∧ ( card ‘ 𝑠 ) = ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) ) → ( ( card ‘ 𝑠 ) ∈ ( card “ 𝑊 ) ∧ ( card ‘ 𝑠 ) = 𝐴 ) ) )
78 77 eximdv ⊢ ( ( CHOICE ∧ ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) = 𝐴 ) → ( ∃ 𝑠 ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ∧ ( card ‘ 𝑠 ) = ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) ) → ∃ 𝑠 ( ( card ‘ 𝑠 ) ∈ ( card “ 𝑊 ) ∧ ( card ‘ 𝑠 ) = 𝐴 ) ) )
79 78 3adant2 ⊢ ( ( CHOICE ∧ ω ≼ 𝐴 ∧ ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) = 𝐴 ) → ( ∃ 𝑠 ( 𝑠 ⊆ ( ( 𝑅1 ‘ 𝐵 ) × ( 𝑅1 ‘ 𝐵 ) ) ∧ 𝑠 We ( 𝑅1 ‘ 𝐵 ) ∧ ( card ‘ 𝑠 ) = ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) ) → ∃ 𝑠 ( ( card ‘ 𝑠 ) ∈ ( card “ 𝑊 ) ∧ ( card ‘ 𝑠 ) = 𝐴 ) ) )
80 27 79 mpd ⊢ ( ( CHOICE ∧ ω ≼ 𝐴 ∧ ( card ‘ ( 𝑅1 ‘ 𝐵 ) ) = 𝐴 ) → ∃ 𝑠 ( ( card ‘ 𝑠 ) ∈ ( card “ 𝑊 ) ∧ ( card ‘ 𝑠 ) = 𝐴 ) )